forall a: forall b:
L:a,b;L:b,a;L:a,b = L:a,b